Inference at * 1 
Iof proof for Lemma b2i bounds:



1. b : 
  (0  b2i(b))  (b2i(b)  1) 

latex

 by ((((BoolCases 1) 
CollapseTHEN (AbReduce 0))) 
CollapseTHEN ((Auto_aux (first_nat 1:n
C) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions

ff, False, P  Q, A, if b then t else f fi , tt, t  T, b2i(b), A  B, P  Q, Unit, ,